Technique: Streams and Corecursion

Programs usually operate over data structures that have a finite size. For example, arrays have a definite end. On the other hand, codata refers to potentially infinite data structures. The simplest example are streams, which are sequences that can go on forever. Programming with codata introduces new challenges—for example, trying to calculate the sum of a stream may lead to a non-terminating computation—but it also enables interesting applications and techniques.

Exact real arithmetic allows us to perform numerical computations to arbitrary precision. This contrasts with floating point numbers, which can produce drastically imprecise results in some cases. In functional programming courses you have probably encountered Peano arithmetic (with Zero and Succ) as one of the fundamental examples for pattern matching and functional programming. Similarily, a digit stream is for example a stream of digits like 0.9999999999.... and arithemtic on digit streams can be considered a fundamental example of working with streams. The idea behind exact real arithmetic is that while we cannot directly represent real numbers, as that would require infinite memory, we can produce streams of better and better approximations and stop when the result is precise enough for us.

Individiual challenges can be to implement

• Interval Arithmetic & Midpoint Arithmetic
• Rational Numbers and Dyadic Rational Numbers
• Shrinking Intervals & Signed Digit Streams
• Eudoxus Numbers
• Algebraic Numbers
• Dedekind vs Cauchy Numbers
• Floats vs Posits.

Many real-world systems continually receive new data which they need to transform, analyze and aggregate. Frameworks like Apache Flink have adopted data streams as the underlying abstraction for implementing such systems.

• A SQL to C compiler in 500 lines of code
• Even Better Stream Fusion

Ideally, a stream computation framework allows programmers to use a high-level, declarative interface, while producing highly efficient code. Techniques from functional programming like higher-order abstract syntax, intrinsically typed embeddings, and smart constructors might be useful for implementing such a framework.

• Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages
• Bottom-up rewriting with smart constructors, hereditary substitution & normalization by evaluation